1. Field of the Invention
This invention relates to implementations of systems as collections of finite state automata, and more particularly to implementations based on formal verification of the correctness of the system being implemented.
2. Description of the Prior Art
A perennial problem in the design of large systems is verifying that the system will indeed behave in the manner intended by its designers. One approach has been simply to try out the system, either by building and testing the system itself or by building and testing a model of it. In recent years, this approach has taken the form of a computer simulation of the system. A computer program which is a model of the system is written, and the system is tested by executing the computer program. A fundamental problem with the approach of "trying out the system" is that the system's designers can only try out behavior which they anticipate. For any but the simplest systems, however, the designers cannot anticipate all of the behavior of the system, and it is of course always unanticipated behavior which causes difficulties.
As the limitations of stimulation have become more apparent, interest has grown in the formal verification of system behavior. In formal verification, the designer provides a logical definition of the system's intended behavior and a logical definition of the implementation to a formal verification system. The formal verification system then determines whether the logical definition of the system's intended behavior implies the logical definition of the implementation. If it does, the implementation is faithful to the logical definition of the intended behavior.
The system described in the parent of the present application is such a formal verification system. However, that system did not deal with real-time delay constraints on system design. A delay constraint specifies a delay by specifying a delay duration which ranges between a minimum delay duration and a maximum delay duration. The minimum delay duration and the maximum delay duration are termed the lower and upper delay bounds respectively.
For example, the system may be required to respond to a stimulus within a fixed period of time. This fixed period is a first delay constraint with a lower delay bound of 0 and an upper delay bound of the fixed period of time. Further, the stimulus may be received by a first one of the automata making up the system and the response may be provided by another one of the automata. Communication between the two automata is by means of a channel which has a second delay constraint in which the lower delay bound specifies the minimum time required to send a message via the channel and the upper delay bound specifies the maximum delay required to send the message. Clearly, if the lower delay bound of the second delay constraint is longer than the upper delay bound of the first delay constraint, the system will always fail; further, if the upper delay bound of the second delay constraint is longer than the upper delay bound of the first delay constraint, the system will fail whenever the condition of the channel is such that the delay required for the message is longer than the upper delay bound of the first delay constraint.
A technique is known for formally verifying whether a system satisfies a set of real-time delay constraints. This technique is set forth in R. Alur and D. L. Dill, "Automata for modeling real-time systems", in Automata, Languages, and Programming: Proceedings of the 17th ICALP, Lecture Notes in Computer Science 443, pp. 322-335, Springer-Verlag, 1990. Unfortunately, there are many cases for which this technique is computationally intractable, and the technique is consequently of limited use in developing implementations of systems. It is thus an object of the invention to provide techniques which are more useful for developing implementations of systems based on formal verification of a system's temporal behavior than those provided by the prior art.